eq_seq(eq)(s1,s2)
== s1/k1,g1. s2/k2,g2. k1=k2  primrec(k1;true;i,b. eq(g1(i),g2(i))  b) 

latex

Definitions	A/x,y. B(x;y), i=j, primrec(n;b;c), true, x.A(x), p  q, f(a)
FDL editor aliases	eq_seq